T:Type, L:(T List), x, y:T. adjacent(T;rev(L);x;y)  adjacent(T;L;y;x) 

latex

Definitions

<a, b>, {T}, i  j , hd(l), Unit, |r|, |g|, |p|, x,y:A//B(x;y), , Atom, , last(L), x =a y, (i = j), [d], a < b, a < b, p q, p  q, b, p  q, x:A.B(x), S  T, Top, ff, , s ~ t, A List, True, Void, n+m, A, null(as), a < b, #$n, ||as||, (xL.P(x)), xL. P(x), x f y, f(a), A c B, a < b, a <p b, a  b, a ~ b, b | a, b, A  B, Dec(P), P  Q, left + right, as @ bs, [car / cdr], rev(as), (x  l), P & Q, {i..j}, P  Q, x:A. B(x), x:A  B(x), [], s = t, P  Q, t  T, False, Type, x:A. B(x), P  Q, adjacent(T;L;x;y), x:AB(x), type List

Lemmas

iff wf, adjacent wf, adjacent-nil, rev implies wf, decidable lt, assert wf, true wf, reverse wf, null append, false wf, top wf, member wf, null wf3, bfalse wf, band wf, assert of null, and functionality wrt iff, assert of band, iff transitivity, not functionality wrt iff, not wf, last wf, length wf1, decidable cand, decidable or, hd wf, adjacent-append, iff functionality wrt iff, adjacent-cons, last-reverse, adjacent-singleton, length-reverse, non neg length